package bcontractor.propositional;

import static org.hamcrest.Matchers.is;
import static org.junit.Assert.assertThat;

import org.junit.Before;
import org.junit.Test;

import bcontractor.propositional.minisat.MiniSatReasoner;

/**
 * Simple tests to ensure the SAT4J SAT reasoner is correctly implemented.
 * 
 * @author lundberg
 * 
 */
public class MiniSatReasonerShould {

	private MiniSatReasoner reasoner;

	private SentenceParser parser;

	@Before
	public void init() {
		this.reasoner = new MiniSatReasonerBuilder().build();
		this.parser = new SentenceParser();
	}

	@Test
	public void testSingleClauseIsSatisfiable() {
		assertThat(this.reasoner.isSatisfiable(this.parser.createSet("a v b")),
				is(true));
	}

	@Test
	public void testSingleClauseIsNotUnsatisfiable() {
		assertThat(
				this.reasoner.isUnsatisfiable(this.parser.createSet("a v b")),
				is(false));
	}

	@Test
	public void testObviousUnsatisfiableIsUnsatisfiable() {
		assertThat(
				this.reasoner.isUnsatisfiable(this.parser.createSet("a ^ ¬a")),
				is(true));
	}

	@Test
	public void testObviousUnsatisfiableIsNotSatisfiable() {
		assertThat(
				this.reasoner.isSatisfiable(this.parser.createSet("a ^ ¬a")),
				is(false));
	}

	@Test
	public void testUnsatisfiableIsUnsatisfiable() {
		assertThat(this.reasoner.isUnsatisfiable(this.parser
				.createSet("(a v b) ^ (a v ¬b) ^ ¬a")), is(true));
	}

	@Test
	public void testUnsatisfiableIsNotSatisfiable() {
		assertThat(this.reasoner.isUnsatisfiable(this.parser
				.createSet("(a v b) ^ (a v ¬b) ^ ¬a")), is(true));
	}

	@Test
	public void testObviousEntailment() {
		assertThat(this.reasoner.entails(this.parser.createSet("¬a v b", "a"),
				this.parser.create("a")), is(true));
	}

	@Test
	public void testObviouslyFalseEntailment() {
		assertThat(this.reasoner.entails(this.parser.createSet("¬a v b", "a"),
				this.parser.create("¬a")), is(false));
	}

	@Test
	public void testDirectEntailment() {
		assertThat(this.reasoner.entails(this.parser.createSet("¬a v b", "a"),
				this.parser.create("b")), is(true));
	}

	@Test
	public void testFalseDirectEntailment() {
		assertThat(this.reasoner.entails(this.parser.createSet("¬a v b", "a"),
				this.parser.create("¬b")), is(false));
	}

	@Test
	public void testIndirectEntailment() {
		assertThat(this.reasoner.entails(this.parser.createSet("¬a v b",
				"¬c v d", "¬b v ¬d v e", "a", "c"), this.parser.create("e")),
				is(true));
	}

	@Test
	public void testFalseIndirectEntailment() {
		assertThat(this.reasoner.entails(this.parser.createSet("¬a v b",
				"¬c v d", "¬b v ¬d v e", "a", "c"), this.parser.create("¬e")),
				is(false));
	}
}
